$\forall$${\it ds}_{1}$, ${\it ds}_{2}$:$x$:Id fp$\rightarrow$ Type. Normal(${\it ds}_{1}$) $\Rightarrow$ Normal(${\it ds}_{2}$) $\Rightarrow$ Normal(${\it ds}_{1}$ $\oplus$ ${\it ds}_{2}$)